1. Technical Field
The present invention relates in general to verifying designs and in particular to performing retiming analysis. Still more particularly, the present invention relates to a system, method and computer program product for performing retiming analysis in the presence of verification constraints.
2. Description of the Related Art
With the increasing penetration of processor-based systems into every facet of human activity, demands have increased on the processor and application-specific integrated circuit (ASIC) development and production community to produce systems that are free from design flaws. Circuit products, including microprocessors, digital signal and other special-purpose processors, and ASICs, have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of error-free and flaw-free design. Whether the impact of errors in design would be measured in human lives or in mere dollars and cents, consumers of circuit products have lost tolerance for results polluted by design errors. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable circuit results has risen to a mission-critical concern.
In response to the increasing need for reliable, error-free designs, the processor and ASIC design and development community has developed rigorous, if incredibly expensive, methods for testing and verification for demonstrating the correctness of a design. The task of hardware verification has become one of the most important and time-consuming aspects of the design process.
Among the available verification techniques, formal and semiformal verification techniques are powerful tools for the construction of correct logic designs. Formal and semiformal verification techniques offer the opportunity to expose some of the probabilistically uncommon scenarios that may result in a functional design failure, and frequently offer the opportunity to prove that the design is correct (i.e., that no failing scenario exists). Unfortunately, formal verification techniques require computational resources which are exponential with respect to the design under test. In particular, many formal analysis techniques require exponential resources with respect to the number of state elements in the design under test. Semi-formal verification techniques leverage formal algorithms on larger designs by applying them only in a resource-bounded manner, though at the expense of incomplete verification coverage. Generally, coverage decreases as design size increases.
Constraints are often used in verification to prune the possible input stimulus in certain states of the design. For example, a constraint may state “if the design's buffer is full, then constrain the input stimulus to prevent new transfers into the design”. Semantically, the verification tool must discard any states for which a constraint evaluates to a 0 (i.e., the verification tool may never produce a failing scenario showing a violation of some property of the design, if that scenario does not adhere to all the constraints for all time-steps prior to the failure). In the previous example, it would be illegal for the verification tool to produce a trace of length “i” showing a violation of some property, if that trace illustrated the scenario that the buffer was full and a new transfer was initiated into the design between time 0 and i (inclusive).
Retiming techniques, initially developed for enhanced synthesis, have more recently been proposed to enhance verification through reduction in state element count. However, prior art retiming algorithms have the problematic propensity to shift every gate in a design under verification by an arbitrary amount, which poses challenges to the use of retiming in a verification setting under the presence of constraints. Specifically, a verification tool may lose the ability to discern whether a trace is “legal” (e.g., adhering to all constraints at all time-steps until the violation of a property), if the property gate and the constraint gate were retimed by different amounts before passing them into the verification tool. No prior art technique addresses how to enable such an application.
Generally speaking, retiming refers to the process of moving state elements across combinational gates. More specifically, a “retiming” of a circuit is a labeling of each of its combinational gates “g” with an integer “r(g)”, where “r(g)” represents the number of state elements (hereafter referred to as “registers”) that were dragged backward (i.e., toward the circuit inputs) across gate g. Referring now to FIG. 3A, an exemplary initial circuit design is depicted. Exemplary initial circuit design 310 has a primary input gate g1 300, which has two sinks: register r1 302, and register r2 306. Register r1 302 in turn has a buffer g2 304 as a sink, and register r2 306 has an inverter gate g3 308 as a sink.
A retiming may label g1 300 with 0, and g2 304 with −1, meaning that the retiming has relocated the register r1 302 “fanout-wise across” g2 304. Hereafter, a negative retiming, which relocates a register fanout-wise across a gate, is referred to as a “forward retiming”. In a verification setting, it is often desirable to solve a retiming problem in such a way that the total number of state elements in the design is minimized. Various prior-art algorithms are available to solve the resulting minimization problem. For example, retiming may be cast as a min-cost flow problem for which the “network simplex” algorithm or an Integer Linear Program solver may be used to obtain a solution.
Retiming in the presence of constraints is a nontrivial problem, as illustrated by the following example. Returning to the example of FIG. 3A, assume g2 304 is a verification “target”, meaning that an attempt is being made to demonstrate whether or not it is possible to drive a logical ‘1’ to g2 304. With no constraints, the prior art, given the semantics of an appropriate netlist (discussed below), allows a verification tool to freely drive a 0 or a 1 value to the primary input gate g1 300. R1 302 will shadow the value on g1 300 one time-step later, while g2 304 always evaluates to the same value as r1 302. However, assuming that g3 308 is labeled as a constraint, meaning that the verification tool may never evaluate that gate to a “0”, prior art methods limit the tool such that the tool cannot evaluate r2 306 to a “1”. Because r1 302 and r2 306 always takes the same value, the target may never be asserted to a “1”.
Referring now to FIG. 3B, an exemplary retimed circuit design which has been retimed from initial circuit design 310 under prior-art techniques is depicted. Exemplary retimed circuit design 312 has a primary input gate g1 320 and still contains register r1 322, register r2 326, buffer g2 324 and an inverter gate g3 328. Retiming initial circuit design 310 relocates r1 322 fanout-wise past g2 324. Such a retiming will alter the semantics of the verification problem as g2 324 takes the same value as g1 320 (without a one time-step delay), and the constraint only “restricts” the behavior of g1 320 one time-step later. The example depicted in FIG. 3A and FIG. 3B demonstrates a key inadequacy of prior art retiming techniques; retiming may take a target which is not assertable appear to be assertable.
It is also noteworthy that the reverse transformation from FIG. 3B to FIG. 3A by relocating r1 322 fanin-wise across g2 324 may additionally make an assertable target appear to be not assertable.
From the example depicted in FIG. 3A and FIG. 3B, it should be realized that in designs with many thousands or million gates, possibly including many target and constraint gates, it becomes very cumbersome and difficult to ensure under the prior art that optimal results obtained from a retiming solver can be guaranteed to adhere to the specified constraints.
What is needed is a sound method to perform retiming in a verification setting under the presence of constraints.